(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?0 : (A : Set) → A → A ?1 : (A B : Set) → A → (A → B) → B ?2 : (A B : Set) → A ∧ B → B ∧ A ?3 : (A B C : Set) → (A ∧ B) ∧ C → A ∧ (B ∧ C) ?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?8 : (A : Set) → A → ¬ (¬ A) ?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : X → Σ X (λ x → ⊤) ?15 : Σ (X → X) (λ x → ⊤) ?16 : Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
(agda2-give-action 0 "λ A z → z")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?1 : (A B : Set) → A → (A → B) → B ?2 : (A B : Set) → A ∧ B → B ∧ A ?3 : (A B C : Set) → (A ∧ B) ∧ C → A ∧ (B ∧ C) ?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?8 : (A : Set) → A → ¬ (¬ A) ?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : X → Σ X (λ x → ⊤) ?15 : Σ (X → X) (λ x → ⊤) ?16 : Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
(agda2-give-action 1 "λ A B z z₁ → z₁ z")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?2 : (A B : Set) → A ∧ B → B ∧ A ?3 : (A B C : Set) → (A ∧ B) ∧ C → A ∧ (B ∧ C) ?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?8 : (A : Set) → A → ¬ (¬ A) ?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : X → Σ X (λ x → ⊤) ?15 : Σ (X → X) (λ x → ⊤) ?16 : Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
(agda2-give-action 2 "λ A B z → ∧-i (_∧_.snd z) (_∧_.fst z)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?3 : (A B C : Set) → (A ∧ B) ∧ C → A ∧ (B ∧ C) ?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?8 : (A : Set) → A → ¬ (¬ A) ?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : X → Σ X (λ x → ⊤) ?15 : Σ (X → X) (λ x → ⊤) ?16 : Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(3 4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
(agda2-give-action 3 "λ A B C z → ∧-i (_∧_.fst (_∧_.fst z)) (∧-i (_∧_.snd (_∧_.fst z)) (_∧_.snd z))")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?8 : (A : Set) → A → ¬ (¬ A) ?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : X → Σ X (λ x → ⊤) ?15 : Σ (X → X) (λ x → ⊤) ?16 : Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
((last . 2) . (agda2-make-case-action '("h4 A B C (∨-i₁ x) h₁ h₂ = h₁ x" "h4 A B C (∨-i₂ x) h₁ h₂ = h₂ x")))
((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
((last . 2) . (agda2-make-case-action '("h5 A B (∨-i₁ x) = ∨-i₂ x" "h5 A B (∨-i₂ x) = ∨-i₁ x")))
((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
((last . 2) . (agda2-make-case-action '("h6 A B C (∨-i₁ (∨-i₁ x)) = ∨-i₁ x" "h6 A B C (∨-i₁ (∨-i₂ x)) = ∨-i₂ (∨-i₁ x)" "h6 A B C (∨-i₂ x) = ∨-i₂ (∨-i₂ x)")))
((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
((last . 2) . (agda2-make-case-action '("h7 A ()")))
((last . 1) . (agda2-goals-action '(4 5 6 7 8 9 10 11 12 13 14 15 16 17)))
(agda2-give-action 8 "λ A z z₁ → z₁ z")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?9 : (A : Set) → ¬ (¬ (¬ A)) → ¬ A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : X → Σ X (λ x → ⊤) ?15 : Σ (X → X) (λ x → ⊤) ?16 : Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(4 5 6 7 9 10 11 12 13 14 15 16 17)))
(agda2-give-action 9 "λ A z z₁ → z (λ z₂ → z₂ z₁)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?10 : ((A : Set) → ¬ (¬ A) → A) → (A : Set) → A ∨ ¬ A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : X → Σ X (λ x → ⊤) ?15 : Σ (X → X) (λ x → ⊤) ?16 : Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(4 5 6 7 10 11 12 13 14 15 16 17)))
(agda2-give-action 10 "λ z A → z (A ∨ ((x : A) → ⊥)) (λ z₁ → z₁ (∨-i₂ (λ x → z₁ (∨-i₁ x))))")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?11 : ((A : Set) → A ∨ ¬ A) → (A : Set) → ¬ (¬ A) → A ?12 : ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : X → Σ X (λ x → ⊤) ?15 : Σ (X → X) (λ x → ⊤) ?16 : Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(4 5 6 7 11 12 13 14 15 16 17)))
(agda2-give-action 11 "λ z A z₁ → ∨-e A ((x : A) → ⊥) A (z A) (λ z₂ → z₂) (λ z₂ → ⊥-e A (z₁ z₂))")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?12 : ((x : X) → P x ∧ Q x) → ((x : X) → P x) ∧ ((x : X) → Q x) ?13 : ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : X → Σ X (λ x → ⊤) ?15 : Σ (X → X) (λ x → ⊤) ?16 : Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(4 5 6 7 12 13 14 15 16 17)))
(agda2-give-action 12 "λ z → ∧-i (λ x → _∧_.fst (z x)) (λ x → _∧_.snd (z x))")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?13 : ((x : X) → P x) ∧ ((x : X) → Q x) → (x : X) → P x ∧ Q x ?14 : X → Σ X (λ x → ⊤) ?15 : Σ (X → X) (λ x → ⊤) ?16 : Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(4 5 6 7 13 14 15 16 17)))
(agda2-give-action 13 "λ z x → ∧-i (_∧_.fst z x) (_∧_.snd z x)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?14 : X → Σ X (λ x → ⊤) ?15 : Σ (X → X) (λ x → ⊤) ?16 : Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(4 5 6 7 14 15 16 17)))
(agda2-give-action 14 "λ x → Σ-i x (record {})")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?15 : Σ (X → X) (λ x → ⊤) ?16 : Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(4 5 6 7 15 16 17)))
(agda2-give-action 15 "Σ-i (λ x → x) (record {})")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?16 : Σ (X → X) (λ f → (x : X) → P (f x) → P x) ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(4 5 6 7 16 17)))
(agda2-give-action 16 "Σ-i (λ x → x) (λ x x₁ → x₁)")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A ?17 : Σ A (λ x → Drink x → Π A Drink) " nil)
((last . 1) . (agda2-goals-action '(4 5 6 7 17)))
(agda2-give-action 17 "RAA (Σ A (λ z → (x : Drink z) → Π A Drink)) (λ z → z (Σ-i a (λ x → fun (λ a → RAA (Drink a) (λ z₁ → z (Σ-i a (λ x₁ → fun (λ a₁ → RAA (Drink a₁) (λ _ → z₁ x₁)))))))))")
(agda2-status-action "")
(agda2-info-action "*All Goals*" "?4 : C ?5 : B ∨ A ?6 : A ∨ (B ∨ C) ?7 : A " nil)
((last . 1) . (agda2-goals-action '(4 5 6 7)))
